\begin{tabbing}
split\_tail($L$ $\mid$ $\forall$$x$.$f$($x$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Ca\=se of $L$\+
\\[0ex]nil $\rightarrow$ $\langle$nil$,\,$nil$\rangle$
\\[0ex]$a$.${\it as}$, rec: $\rightarrow$ \=split\_tail(${\it as}$ $\mid$ $\forall$$x$.$f$($x$))/${\it hs}$,${\it ftail}$.\+
\\[0ex]Ca\=se of ${\it hs}$\+
\\[0ex]nil $\rightarrow$ if $f$($a$)$\rightarrow$ $\langle$nil$,\,$$a$.${\it ftail}$$\rangle$ else $\langle$[$a$]$,\,$${\it ftail}$$\rangle$ fi
\\[0ex]$x$.$y$, rec: $\rightarrow$ $\langle$$a$.${\it hs}$$,\,$${\it ftail}$$\rangle$
\-\-\-\\[0ex]\emph{(recursive)}
\end{tabbing}